T:Type, w:World.
FairFifo  (e:E, x:Id. (vartype(loc(e);x) r T)  (state_after(e)(x) = (x after e)  T)) 

latex

Definitions	s = t, x:AB(x), , loc(e), state_after(e), (x after e), f(a), vartype(i;x), SQType(T), {T}, s ~ t, suptype(S; T), S  T, b, A  B, A, False, state_after(e), <a, b>, , time(e), x,y:A//B(x;y), x,y. t(x;y), , qeq(r;s), tt, EquivRel(T;x,y.E(x;y)), , A  B, , , Id, Atom$n, E, {x:A| B(x)} , FairFifo, P & Q, World, x:A  B(x), Type, P  Q, x:A. B(x), t  T
Lemmas	w-after wf, w state after wf, rationals wf, int nzero wf, b-union wf, btrue wf, qeq wf2, bool wf, quotient wf, int-rational, w-vartype wf, Id wf, w-state-after, w-loc wf, world wf, fair-fifo wf, w-E wf